$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop), $L$:$T$ List.
\\[0ex]0$<\parallel$$L$$\parallel$
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($x$ $=$ $y$))
\\[0ex]$\Rightarrow$ (($\forall$$x$$\in$$L$. $\forall$$y$$\in$$L$. $\neg$$x$ $=$ $y$ $\in$ $T$ $\Rightarrow$ $P$($x$) $\vee$ $P$($y$)) $\Leftrightarrow$ ($\exists$$x$$\in$$L$.$\forall$$y$$\in$$L$. $\neg$$x$ $=$ $y$ $\in$ $T$ $\Rightarrow$ $P$($y$)))